State the assumptions and split the models into MCDisruptor - #232

Both specs require the assumption but neither states it.  The variable
pc holds one program counter per thread id, so an id in both Writers
and Readers shares a single counter between its writer and its reader
role.  Since pc[t] = "Access" is the sole guard of EndWrite and of
EndRead, the Begin action of either role enables the End action of the
other.

In SPMC, EndWrite after BeginRead advances published past a sequence
number that no writer wrote; a consumer then reads the unwritten slot
and appends NULL to the consumed history, which violates TypeOk.  In
MPMC, EndRead after BeginWrite abandons a write in progress and leaves
the writer registered in ringbuffer.writers for that slot; a consumer
that subsequently enters the slot violates NoDataRaces.  Both reports
ascribe a defect of the model to the algorithm.

Producers and consumers are distinct threads in the Disruptor and every
configuration already keeps the two sets disjoint, so the state spaces
are unchanged.  RingBuffer is not the place for the assumption: TLC
ignores the assumptions of an instantiated module, and pc is not
declared there.

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

MaxPublished bounds the model rather than the Disruptor.  The producers
publish without end, and the constant exists solely to keep the
sequence numbers and the consumed history finite.  StateConstraint and
Liveliness are both expressed in terms of it, the latter by quantifying
i over a range that ends at MaxPublished, so the constant, its
assumption MaxPublishedIsPositive, the constraint and the property move
together.  Disruptor_SPMC and Disruptor_MPMC now hold the algorithms
alone, MCDisruptor_SPMC and MCDisruptor_MPMC the models.  The state
spaces are unchanged.

Liveliness moves verbatim.  A comment at its new location records that
TLC checks it on the state graph pruned by StateConstraint, in which a
behavior may terminate in a state whose successors were all pruned; a
positive result is therefore weaker than it appears.

The Apalache wrappers declared MaxPublished and their configurations
assigned it, although both check NoDataRaces alone, under neither the
state constraint nor the property.  The declarations and the
assignments are removed.

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>